(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v9 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const v23 Bool)
(declare-const v29 Bool)
(declare-const i4 Int)
(push)
(assert (or v13 (<= 305 305 (* 749 (- 749 83 659) i2 (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659))) (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659)))) (- (* (- 749 83 659) (- 12 83) 202 659))) (and (not v0) v9 v16 v18 v11 v15)))
(assert (or (and v23 v12 v5 v18 v15 v5 v12) v2 v29))
(assert (and (or (and (not v0) v9 v16 v18 v11 v15) (<= 305 305 (* 749 (- 749 83 659) i2 (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659))) (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659)))) (- (* (- 749 83 659) (- 12 83) 202 659))) v17) (or v6 v29 (<= 305 305 (* 749 (- 749 83 659) i2 (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659))) (- 867 174 i2 (* (- 12 83) 202 0 (* 0 (- 12 83) 202 659)))) (- (* (- 749 83 659) (- 12 83) 202 659)))) (or v29 v13 (and (not v0) v9 v16 v18 v11 v15)) (or (and (not v0) v9 v16 v18 v11 v15) (> (- (* (- 749 83 659) (- 12 83) 202 659)) (- 12 83)) (and (not v0) v9 v16 v18 v11 v15)) (or v29 v6 v2) (or v6 v17 (<= 305 305 0 0)) (or (and (not v0) v9 v16 v18 v11 v15) (and (not v0) v9 v16 v18 v11 v15) (and v23 v12 v5 v18 v15 v5 v12)) (or v17 (<= 305 305 0 0) v17) (or (or v2 v17 (and (not v0) v9 v16 v18 v11 v15)) (or v2 v29 (and v23 v12 v5 v18 v15 v5 v12)) (or v13 (and v23 v12 v5 v18 v15 v5 v12) (<= 305 305 0 0)) (or (and (not v0) v9 v16 v18 v11 v15) (and (not v0) v9 v16 v18 v11 v15) (and v23 v12 v5 v18 v15 v5 v12)) (or v29 v13 (and (not v0) v9 v16 v18 v11 v15)) (or v13 (> (- 0) 0) (and v23 v12 v5 v18 v15 v5 v12)) (or (<= 305 305 (* 749 (- 749 83 659) i2 (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659))) (- 867 174 i2 (* (- 12 83) 202 (* (- 749 83 659) (- 12 83) 202 659) (* (- 749 83 659) (- 12 83) 202 659)))) 0) (and v23 v12 v5 v18 v15 v5 v12) (<= 305 305 0 0))) (or v6 v13 v17)))
(check-sat)
(assert (or (and (not v0) v9 v16 v18 v11 v15) v2 v13))
(check-sat)
